A, B:Type, g:(A(B + Top)), X:MaInterface(A), es:ES.
ma-interface-consistent(es;X)
 ([[ma-interface-compose(g;X)]] = g o [[X]]    AbsInterface(B)) 

latex

Definitions

x:A. B(x), Top, P  Q, AbsInterface(A), [[X]], f o g  , if b then t else f fi , can-apply(f;x), do-apply(f;x), isl(x), t  T, tt, ff, , b, ma-in-interface(es;X;e), ma-interface-val(es;X;e), ma-interface-compose(g;X), p  q, t.2, x. t(x), P & Q, outl(x), , Unit, P  Q, MaInterface(T), ma-interface-consistent(es;X), x(s), ma-interface-consistent-at(es;i;X), False, e@i. P(e), t.1, A c B,

Lemmas

ma-in-interface-compose, ma-in-interface wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-E wf, ma-abs-interface wf, ma-interface-compose wf, ma-interface-consistent-compose, p-compose wf, ma-interface-consistent wf, event system wf, ma-interface wf, top wf, fpf-dom wf, Id wf, id-deq wf, fpf-trivial-subtype-top, fpf wf, Knd wf, hasloc wf, decl-state wf, es-loc wf, fpf-ap wf, es-kind wf, es-hasloc, false wf, Kind-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, alle-at wf, subtype rel wf, es-valtype wf, pi1 wf, es-vartype wf, fpf-cap wf, es-state-when wf, es-state-subtype, es-val wf